00100	INF_PRED: =; EQUALITY: =; PRE_OP:F,G; VAR:x,y,z,u,v,X,Y,Z,U,V,W;
00200	A1:F(F(X,Y,U),V,F(X,Y,W))=F(X,Y,F(U,V,W));
00300	A2:F(Y,X,X)=X;
00400	A3:F(X,Y,G(Y))=X;
00500	THEOREM:F(G(Y),Y,X)=X;
00600	;